$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $f$:$x$:$A$ fp$\rightarrow$ $B$($x$), $C$:Type, $a$:($A$$\rightarrow$($C$+Unit)), $b$:($C$$\rightarrow$$A$).
\\[0ex]($\forall$$y$:$A$. isl($a$($y$)) $\Rightarrow$ $b$(outl($a$($y$))) $=$ $y$) $\Rightarrow$ compose{-}fpf($a$;$b$;$f$) $\in$ $y$:$C$ fp$\rightarrow$ $B$($b$($y$))